package org.eclipse.iota.bounds;

import java.math.BigInteger;

import static org.eclipse.iota.bounds.BoundType.LOWER;
import static org.eclipse.iota.bounds.BoundType.UPPER;

import org.eclipse.iota.model.Clause;
import org.eclipse.iota.model.Constant;
import org.eclipse.iota.model.Equation;
import org.eclipse.iota.model.EquationType;
import org.eclipse.iota.model.Expression;
import org.eclipse.iota.util.IotaCopyUtil;
import org.eclipse.iota.util.IotaReplaceUtil;

/**
 * Utility methods for reasoning about bounds.
 * @author Christian Krause
 * @generated NOT
 */
public class IotaBoundUtil {
	
	/**
	 * Check whether an expression is less than a given constant value
	 * according to the given argument clause. If the method returns 
	 * <code>false</code>, this does not mean that it is greater or equal!
	 * @param expression Expression.
	 * @param value Constant value.
	 * @param clause Clause to be checked.
	 * @return <code>true</code> if it is definitely less.
	 */
	public static boolean isLessThan(Expression expression, Constant value, Clause clause) {
		@SuppressWarnings("deprecation")
		Constant upper = OldIotaBoundCalculator.calculateUpperBound(expression, clause);
		if (upper==null) return false;
		else return upper.isLessThan(value);
	}
	
	/**
	 * Check whether an expression is greater than a given constant value
	 * according to the given argument clause. If the method returns 
	 * <code>false</code>, this does not mean that it is less or equal!
	 * @param expression Expression.
	 * @param value Constant value.
	 * @param clause Clause to be checked.
	 * @return <code>true</code> if it is definitely greater.
	 */
	public static boolean isGreaterThan(Expression expression, Constant value, Clause clause) {
		@SuppressWarnings("deprecation")
		Constant lower = OldIotaBoundCalculator.calculateLowerBound(expression, clause);
		if (lower==null) return false;
		else return lower.isGreaterThan(value);
	}
	
	/**
	 * Check if an expression is positive according to the given argument clause.
	 * @param Expression expression.
	 * @param clause Clause clause.
	 * @return <code>true</code> if it is definitely positive.
	 */
	public static boolean isPositive(Expression expression, Clause clause) {
		return isGreaterThan(expression, ZERO, clause);
	}
	
	/**
	 * Check if an expression is negative according to the given argument clause.
	 * @param expression Expression.
	 * @param clause Clause clause.
	 * @return <code>true</code> if it is definitely negative.
	 */
	public static boolean isNegative(Expression expression, Clause clause) {
		return isLessThan(expression, ZERO, clause);
	}
	
	/**
	 * @deprecated
	 */
	public static Equation makeConstraint(Expression target, Constant bound, BoundType type) {
		Equation equation = new Equation(IotaCopyUtil.copy(target), makeExclusive(bound, type));
		equation.setType(type==BoundType.UPPER ? EquationType.LESS : EquationType.GREATER); 
		return equation;
	}
	
	public static Constant makeExclusive(Constant inclusive, BoundType type) {
		if (type==LOWER) return inclusive.decrease();
		if (type==UPPER) return inclusive.increase();
		return null;
	}
	
	public static Constant makeInclusive(Constant exclusive, BoundType type) {
		return makeExclusive(exclusive, type.flip());
	}
	
	/*
	 * For private use only.
	 */
	private static final Constant ZERO = new Constant(BigInteger.ZERO);
	
}
